g, h:IGroup, f:(|g||h|). (a, b:|g|. f(a * b) = ((f(a)) * (f(b))))  IsMonHom{g,h}(f) 

latex

Up	groups 1
Definitions of Statement	IMonoid, IGroup, IsMonHom{M1,M2}(f)
Definitions	, t  T, FunThru2op(A;B;opa;opb;f), P & Q, IsMonHom{M1,M2}(f), x f y, P  Q, x:A. B(x), P  Q, P  Q, IMonoid, IGroup
Lemmas	igrp wf, grp op wf, grp car wf, grp id wf, grp eq op l, mon ident